Branch for fixing the self-writing bug with overlapping non-identical addresses - #18

GitHub changed its archive tarball generation format, so the
sha256 hashes pinned for the PLSec-VU/pantomime, pantomime-base,
and pantomime-clash GitHub archives no longer matched what GitHub
serves, breaking CI's dependency install step.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

The obligations in Proof.Functional.Induction and Proof.SMT.Sanity are
discharged by the Pantomime plugin while GHC compiles them, so building
those modules needs an SMT solver on PATH. Z3 is the only one packaged
for Ubuntu and does not finish these queries in useful time, which is
why the CI job ran until it was killed rather than failing.

Move the two modules under proof-smt/ and gate them on a new smt-proof
flag, on by default and off in CI, and drop the z3 install from the
workflow. Everything else still runs there: the QuickCheck harness goes
through the same Proof.Functional.Obligation definitions the symbolic
proof does, so CI still checks the obligations on sampled states, along
with driver/driverRef agreement, driver-case coverage and both rv32ui
suites. Locally the flag stays on and bitwuzla discharges all seven
properties in about a minute; package.yaml carries the invocation.

Also add IsaSpec, which runs the ISA model itself against rv32ui. The
refinement proof is stated against ISA, so it cannot say whether ISA is
right; the only check until now was transitive, via the core passing the
same suite, which validates the specification through the implementation.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The obligations derived the whole architectural state from the system
state via isaOfG, which read isaPc off the execute stage. That is only
the conjunct the running case uses to pin it: startup pins it to the
fetch stage and the halted cases to stateHalt. So startup and halted
states satisfied no case of the invariant as a pre-state, and their
obligations held vacuously.

isaPc is a scalar, so the invariant pins it exactly whichever case
applies; only the register file and memory have to be derived, because
the invariant compares those pointwise and a freely quantified pair
would be tied to the system state at just the witness register and byte.
So isaAt takes the PC as an argument and the four indStep properties
quantify over it.

Two consequences. isaOfHop goes away -- it existed solely to patch the
startup case. And k=0 and k=1 can drop "IsaHalted -> True" in favour of
requiring the invariant with the architectural state carried across,
which, since the halted cases demand the architectural register file and
memory equal the core's, says the core stands still once halted. That
was previously established only by reading Core.hs.

hopPc replaces isaOfHop for the callers that need a concrete
architectural state rather than a quantified one: the leakage projection
and the QuickCheck harness.

Admitting startup states also turned up a bug in inductiveStep, which
had been skipping them all along because isaOfG gave them a PC no case
admits. It advanced the ISA across a startup hop, which retires nothing;
indStepObligation1 already carved that case out.

All seven symbolic properties re-discharged under bitwuzla; 143 tests
pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Nothing in Haskell applies the constructor: the plugin synthesises a
KState as a fresh symbolic input to each property, and sysOf only reads
it back through the field accessors, so -Wunused-top-binds sees a dead
constructor. Exporting it says what is actually true -- the type is part
of this module's interface -- rather than suppressing the warning.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

invAtFree compared the architectural memory and register file against
flushMemByteAt and flushRfWordAt, hand-written pointwise re-encodings of
flushMeStage/flushWbStage. Their stated purpose was to spare the solver a
select over a nested store chain, but isaAt already applies the real
flush in every obligation, so that chain is in every query regardless.

The copies only added risk. flushMemByteAt's four-way byte mux had to
agree with memWriteWord, and flushRfWordAt's memory-over-writeback
priority with the flush ordering, and the only check on either was the
sampled fold-free/list agreement test, whose witness addresses step by
16 and so barely reach three of the four mux branches.

runningCaseAt now applies flushMeStage . flushWbStage and reads the
result at the witness, the same flush the container form compares whole.

All seven obligations re-discharged under bitwuzla; solver time moved
from 132s to 144s in single runs, within noise. 143 tests pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Each inductive step's conclusion repeated invAtFree inside both arms of a
case on isaStep, so it took reading both arms to see that they differ only
in the architectural state. Bind that state as isa' first; the conclusion
is then a single invAtFree call against the stepped system state. In k=1
the startup carve-out moves into isa' too, where it reads as what it is:
a startup hop carries the architectural state across unchanged.

No change in meaning. All seven obligations re-discharged under bitwuzla;
143 tests pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

When ISAStep was merged into ISA, every importer was given the same full
explicit list, so six modules imported names they never use and GHC
warned about each. Trim every list to what the module actually refers to.

No change in behaviour: 0 errors, no remaining ISA import warnings, and
133 tests pass in the no-solver configuration.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The invariant had a startup case relating the reset state to the ISA's
initial state. It made k=1 the one step that retires no instruction, so
indStepObligation1 and the QuickCheck harness both needed an
isStartupShape carve-out.

Drop the startup case. The reset state is not related to the ISA at all;
instead baseCase states the reset hop directly: the driver gives the reset
state a two-cycle hop, and after those two core steps and zero ISA steps
the running case holds. Every inductive step now retires exactly one
instruction, so the carve-outs go.

On the test side the concrete base case checks the same on the real reset
state, including that stepping operationally agrees the hop is two cycles.
invTrace no longer lists the reset state among the states the invariant is
checked at, and the startup generator and its tests are removed.
isStartupShape stays for hopPc and the leakage projection. The invariant
note is updated to match.

All seven obligations re-discharged under bitwuzla; 142 tests pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The ecall halted case wrote Core.Syscall while the ebreak case wrote a bare
EBreak. The qualification guards against ISA's Instr constructor of the same
name, but that has never been in scope in this module: it imported ISAStep
originally and now takes only IsaStateG and IsaState from ISA. So a bare
Syscall already resolves to Core's HaltState constructor, and the two cases
now read alike.

No change in meaning: an ambiguous or wrongly resolved Syscall would not
compile. No-solver configuration builds cleanly; 132 tests pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Invariant defined isArithOrJumpInstr, the note's predicate, while its
partner isMemInstr lives in Proof.Driver, and nothing in the invariant or
the obligations used it: the running case states "not an environment
instruction" directly. Its only caller was a test checking that the two
predicates partition the non-environment instructions, which justified
collapsing the note's four running cases into that form.

Drop the definition, that test and its allInstrs helper. The note keeps
the predicate as part of the specification; the collapse now rests on
reading the two short case analyses rather than on a check that would
only have caught a mismatch if allInstrs had been kept in step anyway.

No-solver configuration builds cleanly with no new warnings; 131 tests
pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Since "Replace z3 with bitwuzla in CI", the workflow installs bitwuzla and
runs stack test with the smt-proof flag on, so the comment claiming CI
builds with the flag off was out of date. Also correct "seconds each" to
"under a minute": indStep3 takes about 50s.

Comment-only change.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>